Definitions | i <z j, i z j, t T, type List, s = t, Type, x:A B(x), s ~ t, x:A. B(x), as @ bs, ||as||, nth_tl(n;as), [car / cdr], #$n, n+m, , a < b, n - m, i j , {T}, P  Q, SQType(T), ff, , b,  b, True, A B, tt, tl(l), x:A B(x), P & Q, P   Q, T, P  Q, A, (i = j), x =a y, null(as), a < b, f(a), x f y, a < b, [d] , p   q, p  q, p  q, , Unit, left + right |